Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,n__from(n__s(X)))
2:    2ndspos(0,Z)  → rnil
3:    2ndspos(s(N),cons(X,n__cons(Y,Z)))  → rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z)))
4:    2ndsneg(0,Z)  → rnil
5:    2ndsneg(s(N),cons(X,n__cons(Y,Z)))  → rcons(negrecip(activate(Y)),2ndspos(N,activate(Z)))
6:    pi(X)  → 2ndspos(X,from(0))
7:    plus(0,Y)  → Y
8:    plus(s(X),Y)  → s(plus(X,Y))
9:    times(0,Y)  → 0
10:    times(s(X),Y)  → plus(Y,times(X,Y))
11:    square(X)  → times(X,X)
12:    from(X)  → n__from(X)
13:    s(X)  → n__s(X)
14:    cons(X1,X2)  → n__cons(X1,X2)
15:    activate(n__from(X))  → from(activate(X))
16:    activate(n__s(X))  → s(activate(X))
17:    activate(n__cons(X1,X2))  → cons(activate(X1),X2)
18:    activate(X)  → X
There are 20 dependency pairs:
19:    FROM(X)  → CONS(X,n__from(n__s(X)))
20:    2ndspos#(s(N),cons(X,n__cons(Y,Z)))  → ACTIVATE(Y)
21:    2ndspos#(s(N),cons(X,n__cons(Y,Z)))  → 2ndsneg#(N,activate(Z))
22:    2ndspos#(s(N),cons(X,n__cons(Y,Z)))  → ACTIVATE(Z)
23:    2ndsneg#(s(N),cons(X,n__cons(Y,Z)))  → ACTIVATE(Y)
24:    2ndsneg#(s(N),cons(X,n__cons(Y,Z)))  → 2ndspos#(N,activate(Z))
25:    2ndsneg#(s(N),cons(X,n__cons(Y,Z)))  → ACTIVATE(Z)
26:    PI(X)  → 2ndspos#(X,from(0))
27:    PI(X)  → FROM(0)
28:    PLUS(s(X),Y)  → S(plus(X,Y))
29:    PLUS(s(X),Y)  → PLUS(X,Y)
30:    TIMES(s(X),Y)  → PLUS(Y,times(X,Y))
31:    TIMES(s(X),Y)  → TIMES(X,Y)
32:    SQUARE(X)  → TIMES(X,X)
33:    ACTIVATE(n__from(X))  → FROM(activate(X))
34:    ACTIVATE(n__from(X))  → ACTIVATE(X)
35:    ACTIVATE(n__s(X))  → S(activate(X))
36:    ACTIVATE(n__s(X))  → ACTIVATE(X)
37:    ACTIVATE(n__cons(X1,X2))  → CONS(activate(X1),X2)
38:    ACTIVATE(n__cons(X1,X2))  → ACTIVATE(X1)
The approximated dependency graph contains 4 SCCs: {34,36,38}, {21,24}, {29} and {31}. Hence the TRS is terminating.
Tyrolean Termination Tool  (1.01 seconds)   ---  May 3, 2006